Nuprl Lemma : l-union_wf 0,22

T:Type, eq:EqDecider(T), asbs:T List. l-union(eq;as;bs T List 
latex


DefinitionsType, t  T, x:AB(x), EqDecider(T), type List, insert(a;L), x.A(x), reduce(f;k;as), l-union(eq;as;bs)
Lemmasreduce wf, insert wf, deq wf

origin